es:ES, A:Type, k:Knd, l:IdLnk, tg:Id, B:Type, ds:x:Id fp Type,
f:(z:(x:Id. vartype(source(l);x)  ds(x)?Top). 
f:({e:E| loc(e) = source(l)  Id & valtype(e)  A }(B+Unit)).
state dsk:A sends [tg, e.f(e):B] on l  Prop 

latex

Definitions

t  T, x:A. B(x), E, s = t, x:AB(x), P & Q, A & B, {T}, P  Q, sender(e), A/x,y. B(x;y), 1of(t), b, Type, x:AB(x), kind(e), Knd, rcv(l,tg), e@i. P(e), if b t else f fi, ES, left+right, IdLnk, Atom$n, Id, a:A fp B(a), x:A. B(x), Case b of inl(x)  s(x) ; inr(y)  t(y), valtype(e), source(l), loc(e), {x:A| B(x) }, <a,b>, f(a), Unit, x(s), outl(x), val(e), isl(x), , Prop, x:A. B(x), x. t(x), Top, IdDeq, x.A(x), f(x)?z, vartype(i;x), state dsk:A sends [tg, e.f(e):B] on l

Lemmas

fpf wf, IdLnk wf, event system wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, alle-at wf, assert wf, isl wf, es-val wf, outl wf, unit wf, Id wf, es-loc wf, lsrc wf, es-valtype wf, rcv wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, es-E wf